00100	
00200	
00300	(DEFPROP TRYIT 
00400	 (LAMBDA NIL
00500	  (PROG (Z1 Z2 R M)
00600		(SETQ CNT (ADD1 (LENGTH CLAUSES)))
00700		(SETQ EE (CDR EE))
00800	   TRY3 (SETQ Z1 (CAR EE))
00900		(COND ((NOT (HERE Z1)) (GO TRY7)))
01000		(SETQ M (CHOICE Z1))
01100		(COND ((NULL M) (GO TRY7)))
01200	   TRY2 (SETQ Z2 (CAR M))
01300		(COND ((NOT (HERE Z1)) (GO TRY7)) ((NOT (HERE Z2)) (GO TRY8)))
01400	   TRY1 TRY1A
01500		(COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)))
01600		(SETQ R (RESOLVE Z1 Z2))
01700		(COND ((NULL R) (GO TRY6)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
01800		(SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
01900	   TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY8)))
02000		(SETQ R (PARMOD Z1 Z2))
02100		(COND ((NULL R) (GO TRY8)))
02200		(SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
02300	   TRY8 (COND ((TTYIN) (UPDATE CLAUSES) (SETQ CNT (ADD1(LENGTH CLAUSES)))))
02400		(SETQ M (CDR M))
02500		(COND (M (GO TRY2)))
02600	   TRY7 (SETQ EE (CDR EE))
02700		(COND ((NOT (EQ EE (CDR EE1))) (GO TRY3)))
02800		(PRINT (QUOTE COUNT))
02900		(PRINT COUNT)
03000		(PRINT (QUOTE LEVEL))
03100		(PRINT LVL)
03200		(SETQ LVL (ADD1 LVL))
03300		(PRINT (QUOTE ELAPSED-TIME))
03400		(PRINT (TIMEIT))
03500		(COND ((CDR EE1) (SETQ EE1 (LAST EE1)) (GO TRY3)))
03600		(PRINT (QUOTE NO-PROOF-FOUND))
03700		(COND (AUTO (ERR (QUOTE NOPROOF))))
03800		(UPDATE CLAUSES)
03900		(COND ((CDR EE1) (SETQ EE (CDR EE1)) (SETQ EE1 (LAST EE1)) (GO TRY3)))
04000		(ERR (QUOTE NOPROOF)))) 
04100	EXPR)